nLab pseudo-equivalence relation

Redirected from "pseudo-equivalence relations".

Contents

Idea

A pseudo-equivalence relation is like an equivalence relation, but where we allow more than one element in the relation; i.e. the underlying directed graph of the relation is a directed pseudograph. In the same way that magmoids are the raw structure used to build semicategories and categories, sets with pseudo-equivalence relations are the raw structure used to build dagger categories and groupoids (i.e. a groupoid without associativity, unital laws, and inverse laws).

Sets equipped with pseudo-equivalence relations are sometimes called setoids (i.e. in Wilander (2012), §4; Palmgren & Wilander (2014), §2, §6; Emmenegger & Palmgren (2020), §6; Cipriano (2020), Def. 1.1.1), but the term “setoid” is also used in mathematics to refer only to the sets with equivalence relations. In this article, the term “setoid” is used in the former sense of “sets equipped with pseudo-equivalence relations”.

Definition

With a family of sets

Using graph theoretic terminology, a pseudo-equivalence relation on a set VV of vertices is a family of sets E(a,b)E(a, b) of edges for each vertex aVa \in V and bVb \in V, which comes with the following additional structure

  • for each vertex aVa \in V an element

    refl(a)E(a,a)\mathrm{refl}(a) \in E(a, a)
  • for each vertex aVa \in V and bVb \in V a family of functions

    sym(a,b):E(a,b)E(b,a)\mathrm{sym}(a, b):E(a, b) \to E(b, a)
  • for each vertex aVa \in V, bVb \in V, and cinVc \inV, a family of functions

    trans(a,b,c):(E(a,b)×E(b,c))E(a,c)\mathrm{trans}(a, b, c):(E(a, b) \times E(b, c)) \to E(a, c)

With a set

A pseuodo-equivalence relation on a set VV is a set EE and functions s:EVs:E \to V, t:EVt:E \to V (a loop directed pseudograph), with with functions refl:VE\mathrm{refl}:V \to E, sym:EE\mathrm{sym}:E \to E, and

trans:{(f,g)E×E|t(f)= Vs(g)}E\mathrm{trans}:\{(f,g) \in E \times E \vert t(f) =_V s(g)\} \to E

such that

  • for every aVa \in V, s(refl(a))= Eas(\mathrm{refl}(a)) =_E a
  • for every aVa \in V, t(refl(a))= Eat(\mathrm{refl}(a)) =_E a
  • for every fEf \in E, s(f)= Vt(sym(f))s(f) =_V t(\mathrm{sym}(f))
  • for every fEf \in E, t(f)= Vs(sym(f))t(f) =_V s(\mathrm{sym}(f))
  • for every fEf \in E and gEg \in E such that t(f)= Vs(g)t(f) =_V s(g), s(trans(f,g))= Es(f)s(\mathrm{trans}(f,g)) =_E s(f)
  • for every fEf \in E and gEg \in E such that t(f)= Vs(g)t(f) =_V s(g), t(trans(f,g))= Et(g)t(\mathrm{trans}(f,g)) =_E t(g)

Extensional functions, dagger functors, and isomorphisms

We define an extensional function f:ABf:A \to B between two sets AA and BB with pseudo-equivalence relations (E A,refl A,sym A,trans A)(E_A, \mathrm{refl}_A, \mathrm{sym}_A, \mathrm{trans}_A) and (E B,refl B,sym B,trans B)(E_B, \mathrm{refl}_B, \mathrm{sym}_B, \mathrm{trans}_B) to be a function f V:ABf_V:A \to B and a family of functions f E(a,b):E A(a,b)E B(f V(a),f V(b))f_E(a, b):E_A(a, b) \to E_B(f_V(a), f_V(b))

Composition of extensional functions is defined as composition of the vertex function and of each edge function.

An extensional function between two sets with pseudo-equivalence relations is full if every edge function f E(a,b):E A(a,b)E B(f V(a),f V(b))f_E(a, b):E_A(a, b) \to E_B(f_V(a), f_V(b)) is a surjection, and an extensional function is faithful if every edge function is an injection. An extensional function is injective-on-objects? if the vertex function f V:V AV Bf_V:V_A \to V_B is an injection, surjective-on-objects if the vertex function is a surjection, and bijective-on-objects if the vertex function is a bijection.

An extensional function is a dagger functor if additionally it preserves the functions refl\mathrm{refl}, sym\mathrm{sym}, trans\mathrm{trans}

f E(a,a)(refl A(a))=refl B(f V(a))f_E(a, a)(\mathrm{refl}_A(a)) = \mathrm{refl}_B(f_V(a))
f E(a,b)(sym A(a,b)(f))=sym B(f V(a),f V(b))(f E(a,b)(f))f_E(a, b)(\mathrm{sym}_A(a, b)(f)) = \mathrm{sym}_B(f_V(a), f_V(b))(f_E(a, b)(f))
f E(a,c)(trans A(f,g))=trans B(f E(a,b)(f),f E(b,c)(g)f_E(a, c)(\mathrm{trans}_A(f,g)) = \mathrm{trans}_B(f_E(a, b)(f), f_E(b, c)(g)

An isomorphism of setoids is a full and faithful bijective-on-objects dagger functor.

Equivalence of definitions

Given a one-set-of-edges setoid EVE\rightrightarrows V, we define a family-of-sets-of-edges setoid by taking E(x,y)E(x,y) to be the preimage of (x,y)(x,y) under the function (s,t):EV×V(s,t):E \to V\times V. Conversely, given a family-of-sets-of-edges setoid we define a one-set-of-edges setoid by taking EE to be the disjoint union of the families of edges E= x,yVE(x,y)E = \coprod_{x,y\in V} E(x,y).

Examples

The morphisms E(a,b)E(a, b) of a category VV with a contravariant endofunctor that is the identity-on-objects is a pseudo-equivalence relation where

  • for every vertex aVa \in V, bVb \in V, cVc \in V, and dVd \in V and edge fE(a,b)f \in E(a, b), gE(b,c)g \in E(b, c), and hE(c,d)h \in E(c, d)

    trans(a,b,d)(f,trans(b,c,d)(g,h))=trans(a,c,d)(trans(a,b,c)(f,g),h)\mathrm{trans}(a, b, d)(f, \mathrm{trans}(b, c, d)(g, h)) = \mathrm{trans}(a, c, d)(\mathrm{trans}(a, b, c)(f, g), h)
  • for every vertex aVa \in V, bVb \in V and edge fE(a,b)f \in E(a, b)

    trans(a,b,b)(f,refl(b))=f\mathrm{trans}(a, b, b)(f, \mathrm{refl}(b)) = f
  • for every vertex aVa \in V, bVb \in V and edge fE(a,b)f \in E(a, b)

    trans(a,a,b)(refl(a),f)=f\mathrm{trans}(a, a, b)(\mathrm{refl}(a), f) = f

This includes dagger categories, where additionally

  • for every vertex aVa \in V, bVb \in V and edge fE(a,b)f \in E(a, b)

    sym(a,b)(sym(b,a)(f))=f\mathrm{sym}(a, b)(\mathrm{sym}(b, a)(f)) = f
  • for every vertex aVa \in V, bVb \in V, cVc \in V and edge fE(a,b)f \in E(a, b), gE(b,c)g \in E(b, c)

    sym(a,c)(trans(a,b,c)(f,g))=trans(c,b,a)(sym(a,b)(f),sym(b,c)(g))\mathrm{sym}(a, c)(\mathrm{trans}(a, b, c)(f, g)) = \mathrm{trans}(c, b, a)(\mathrm{sym}(a, b)(f), \mathrm{sym}(b, c)(g))
  • for every vertex aVa \in V

    sym(a,a)(refl(a))=refl(a)\mathrm{sym}(a, a)(\mathrm{refl}(a)) = \mathrm{refl}(a)

and groupoids, where

  • for every vertex aVa \in V, bVb \in V and edge fE(a,b)f \in E(a, b)

    trans(a,b,a)(f,sym(a,b)(f))=refl(a)\mathrm{trans}(a, b, a)(f, \mathrm{sym}(a, b)(f)) = \mathrm{refl}(a)
  • for every vertex aVa \in V, bVb \in V and edge f:E(a,b)f:E(a, b)

    trans(b,a,b)(sym(a,b)(f),f)=refl(b)\mathrm{trans}(b, a, b)(\mathrm{sym}(a, b)(f), f) = \mathrm{refl}(b)

Additionally, a pseudo-equivalence relation on a set with one vertex is equivalent to a pointed magma with an endofunction.

Thin setoids

Recall in graph theory that a loop directed pseudograph is simple or a loop digraph if for every vertex aVa \in V and bVb \in V, the set of edges E(a,b)E(a, b) is a subsingleton: for every edge fE(a,b)f \in E(a, b) and gE(a,b)g \in E(a, b), f=gf = g. In the other definition, a loop directed pseudograph is a loop digraph if the functions s:EVs:E \to V and t:EVt:E \to V are jointly monic.

A setoid is thin or simple if its underlying loop directed pseudograph is a loop digraph. In both cases, the pseudo-equivalence relation becomes an equivalence relation. The term “thin” originates from category theory, while the term “simple” originates from graph theory.

A thin setoid is equivalently a thin dagger category, or a dagger category enriched in truth values. A thin setoid is also a thin groupoid, or a groupoid enriched in truth values.

Sometimes in the mathematical literature, setoids are thin by default.

Core of a pseudo-equivalence relation

For any pseudo-equivalence relation AA, the core of AA is defined as the maximal subgroupoid? Core(A)\mathrm{Core}(A) of AA.

More specifically, a sub-pseudo-equivalence relation of a pseudo-equivalence relation AA is a set GG with a pseudo-equivalence relation and an faithful injective-on-objects dagger functor f:GAf:G \to A. A sub-pseudo-equivalence relation GG of AA is a subgroupoid if GG additionally satisfy the groupoid equational axioms:

  • for every vertex aV Ga \in V_G, bV Gb \in V_G, cV Gc \in V_G, and dV Gd \in V_G and edge fE G(a,b)f \in E_G(a, b), gE G(b,c)g \in E_G(b, c), and hE G(c,d)h \in E_G(c, d)

    trans(a,b,d)(f,trans(b,c,d)(g,h))=trans(a,c,d)(trans(a,b,c)(f,g),h)\mathrm{trans}(a, b, d)(f, \mathrm{trans}(b, c, d)(g, h)) = \mathrm{trans}(a, c, d)(\mathrm{trans}(a, b, c)(f, g), h)
  • for every vertex aV Ga \in V_G, bV Gb \in V_G and edge fE G(a,b)f \in E_G(a, b)

    trans(a,b,b)(f,refl(b))=f\mathrm{trans}(a, b, b)(f, \mathrm{refl}(b)) = f
  • for every vertex aV Ga \in V_G, bV Gb \in V_G and edge fE G(a,b)f \in E_G(a, b)

    trans(a,a,b)(refl(a),f)=f\mathrm{trans}(a, a, b)(\mathrm{refl}(a), f) = f
  • for every vertex aV Ga \in V_G, bV Gb \in V_G and edge fE G(a,b)f \in E_G(a, b)

    trans(a,b,a)(f,sym(a,b)(f))=refl(a)\mathrm{trans}(a, b, a)(f, \mathrm{sym}(a, b)(f)) = \mathrm{refl}(a)
  • for every vertex aV Ga \in V_G, bV Gb \in V_G and edge f:E G(a,b)f:E_G(a, b)

    trans(b,a,b)(sym(a,b)(f),f)=refl(b)\mathrm{trans}(b, a, b)(\mathrm{sym}(a, b)(f), f) = \mathrm{refl}(b)

Every pseudo-equivalence relation has at least one subgroupoid given by only the identity morphisms refl(a):E A(a,a)\mathrm{refl}(a):E_A(a, a) of AA. A subgroupoid GG of a pseudo-equivalence relation AA is a maximal subgroupoid if the dagger functor f:GAf:G \to A is bijective-on-objects, and additionally if, for every other subgroupoid HH of AA with faithful injective-on-objects dagger functor g:HAg:H \to A, there is a unique faithful injective-on-objects dagger functor h:HGh:H \to G such that hf=gh \circ f = g.

Category of pseudo-equivalence relations

Let the category Set Set be defined as a category that is finitely complete and well-pointed (i.e. whose terminal object is a extremal generating object). This category of sets is not even a regular category, let alone an exact category, as can happen in certain foundations of mathematics, such as bare set-level Martin-Löf type theory, or ZFC and ETCS without the powerset axiom. The category PseudoEquivRel\mathrm{PseudoEquivRel} of sets with pseudo-equivalence relations is then the ex/lex completion of Set.

More specifically, using the definition of pseudo-equivalence relation with two sets: if (s R,t R):RX(s_R, t_R):R\rightrightarrows X and (s S,t S):SY(s_S, t_S):S\rightrightarrows Y are two pseudo-equivalence relations, a morphism between them in PseudoEquivRel\mathrm{PseudoEquivRel} is defined to be a function f:XYf:X\to Y with functions f 1:RSf_1:R \to S with s Sf 1=fs Rs_S \circ f_1 = f \circ s_R and t Sf 1=ft Rt_S \circ f_1 = f \circ t_R. Moreover, we declare two such functions f,g:XYf,g:X\to Y to be equal if there exists a function h:XSh:X\to S such that sh=fs \circ h = f and th=gt \circ h = g. Because (s S,t S):SY(s_S, t_S):S\rightrightarrows Y is a pseudo-equivalence relation, this defines an actual equivalence relation on the morphisms f:XYf:X\to Y, which is compatible with composition; thus we have a well-defined category PseudoEquivRel\mathrm{PseudoEquivRel} of pseudo-equivalence relations, which is the ex/lex completion of SetSet.

We have a full and faithful functor SetPseudoEquivRelSet\to \mathrm{PseudoEquivRel} sending an object XX to the pseudo-equivalence relation (s X,t X):XX(s_X, t_X):X\rightrightarrows X. One can then verify directly that PseudoEquivRel\mathrm{PseudoEquivRel} is exact, that this embedding preserves finite limits, and that it is universal with respect to lex functors from SetSet into exact categories.

If the presentation axiom (a weak form of the full axiom of choice) holds in SetSet, as a subcategory of PseudoEquivRel\mathrm{PseudoEquivRel}, SetSet could be thought of as the category of completely presented sets, the category of sets with a projective presentation. If the axiom of choice holds in SetSet, then SetSet is equivalent to PseudoEquivRel\mathrm{PseudoEquivRel}, as the axiom of choice implies that SetSet is its own free exact completion, and SetSet is equivalent to PseudoEquivRel\mathrm{PseudoEquivRel} because the free functor from SetSet to PseudoEquivRel\mathrm{PseudoEquivRel} is an equivalence of categories.

This construction could be generalized to any finitely complete category CC, from which the category of internal pseudo-equivalence relations of CC is the ex/lex completion of CC, and denoted as C ex/lexC_{ex/lex}. If every epimorphism in CC is additionally a split epimorphism, then CC is its own free exact completion.

In type theory

Many set-level type theories use types which are 0-truncated and thus h-sets by default because of the inclusion of uniqueness of identity proofs or axiom K to the rule system of the type theory. Sometimes, these type theories do not have quotients and image factorizations, and as a result, setoids are used instead of the native h-sets.

In homotopy type theory, and more generally in any intensional type theory where not all types are h-sets, such as in a type theory without uniqueness of identity proofs or axiom K, the notion of “setoid” bifurcates into multiple distinct notions. In analogy with category, the definitions used above in this article could be called a strict setoid. When the vertex types are only required to be a type rather than a set, then this defines a presetoid. There is also the notion of a univalent setoid, where equality of vertices is isomorphism of vertices in the core of a presetoid.

algebraic structureoidification
magmamagmoid
pointed magma with an endofunctionsetoid/Bishop set
unital magmaunital magmoid
quasigroupquasigroupoid
looploopoid
semigroupsemicategory
monoidcategory
anti-involutive monoiddagger category
associative quasigroupassociative quasigroupoid
groupgroupoid
flexible magmaflexible magmoid
alternative magmaalternative magmoid
absorption monoidabsorption category
cancellative monoidcancellative category
rigCMon-enriched category
nonunital ringAb-enriched semicategory
nonassociative ringAb-enriched unital magmoid
ringringoid
nonassociative algebralinear magmoid
nonassociative unital algebraunital linear magmoid
nonunital algebralinear semicategory
associative unital algebralinear category
C-star algebraC-star category
differential algebradifferential algebroid
flexible algebraflexible linear magmoid
alternative algebraalternative linear magmoid
Lie algebraLie algebroid
monoidal poset2-poset
strict monoidal groupoid?strict (2,1)-category
strict 2-groupstrict 2-groupoid
strict monoidal categorystrict 2-category
monoidal groupoid(2,1)-category
2-group2-groupoid/bigroupoid
monoidal category2-category/bicategory

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

References

For setoids defined as a set with an pseudo-equivalence relation:

Last revised on July 7, 2023 at 18:15:07. See the history of this page for a list of all contributions to it.